Problem:
 0(1(2(2(x1)))) -> 0(1(0(2(2(x1)))))
 0(1(2(2(x1)))) -> 0(1(2(3(2(x1)))))
 0(1(2(2(x1)))) -> 0(2(2(1(3(x1)))))
 0(1(2(2(x1)))) -> 1(0(3(2(2(x1)))))
 0(1(2(2(x1)))) -> 1(2(0(3(2(x1)))))
 0(1(2(2(x1)))) -> 1(3(0(2(2(x1)))))
 0(1(2(2(x1)))) -> 1(3(2(0(2(x1)))))
 0(1(2(2(x1)))) -> 0(1(0(4(2(2(x1))))))
 0(1(2(2(x1)))) -> 0(2(1(3(2(3(x1))))))
 0(1(2(2(x1)))) -> 1(2(1(0(4(2(x1))))))
 0(1(2(2(x1)))) -> 1(5(0(4(2(2(x1))))))
 0(1(2(2(x1)))) -> 2(0(3(1(3(2(x1))))))
 0(1(2(2(x1)))) -> 2(1(1(0(4(2(x1))))))
 0(1(2(2(x1)))) -> 2(1(3(0(2(0(x1))))))
 0(1(2(2(x1)))) -> 2(1(3(3(2(0(x1))))))
 0(1(2(2(x1)))) -> 2(1(5(3(0(2(x1))))))
 0(1(2(2(x1)))) -> 2(2(1(3(0(5(x1))))))
 0(1(2(2(x1)))) -> 2(4(1(3(2(0(x1))))))
 0(1(4(5(x1)))) -> 1(5(0(4(1(x1)))))
 0(1(4(5(x1)))) -> 5(0(4(1(5(x1)))))
 0(1(4(5(x1)))) -> 5(4(1(5(0(x1)))))
 0(1(4(5(x1)))) -> 1(1(5(0(4(1(x1))))))
 0(1(4(5(x1)))) -> 5(4(1(5(5(0(x1))))))
 5(1(2(2(x1)))) -> 1(0(2(2(5(x1)))))
 5(1(2(2(x1)))) -> 1(3(5(2(2(x1)))))
 5(1(2(2(x1)))) -> 1(5(2(3(2(x1)))))
 5(1(2(2(x1)))) -> 1(5(0(2(2(3(x1))))))
 5(1(2(2(x1)))) -> 2(1(0(3(2(5(x1))))))
 5(1(2(2(x1)))) -> 3(1(3(5(2(2(x1))))))
 5(1(2(2(x1)))) -> 4(1(3(2(2(5(x1))))))
 5(1(2(2(x1)))) -> 5(1(0(4(2(2(x1))))))
 5(1(2(2(x1)))) -> 5(1(2(0(4(2(x1))))))
 0(1(1(4(5(x1))))) -> 3(1(0(4(1(5(x1))))))
 0(1(2(2(2(x1))))) -> 1(0(2(2(5(2(x1))))))
 0(1(2(2(5(x1))))) -> 1(5(0(4(2(2(x1))))))
 0(1(2(4(5(x1))))) -> 2(5(1(0(4(5(x1))))))
 0(1(4(5(2(x1))))) -> 1(0(4(2(0(5(x1))))))
 0(1(4(5(5(x1))))) -> 5(0(4(0(1(5(x1))))))
 0(1(5(4(5(x1))))) -> 1(5(0(4(1(5(x1))))))
 0(5(1(2(2(x1))))) -> 0(1(3(2(5(2(x1))))))
 3(3(1(2(2(x1))))) -> 1(3(2(0(3(2(x1))))))
 3(4(4(0(5(x1))))) -> 3(5(4(5(0(4(x1))))))
 5(0(1(2(2(x1))))) -> 1(3(2(0(5(2(x1))))))
 5(1(2(2(5(x1))))) -> 1(5(2(3(2(5(x1))))))
 5(2(1(2(2(x1))))) -> 2(1(3(5(2(2(x1))))))
 5(2(4(0(5(x1))))) -> 0(4(2(5(5(5(x1))))))
 5(2(4(0(5(x1))))) -> 0(4(5(4(2(5(x1))))))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {6,5,4}
   transitions:
    21(60) -> 61*
    21(35) -> 36*
    21(117) -> 118*
    21(77) -> 78*
    21(7) -> 8*
    21(221) -> 222*
    21(211) -> 212*
    21(166) -> 167*
    21(36) -> 37*
    21(31) -> 32*
    21(223) -> 224*
    21(21) -> 22*
    21(188) -> 189*
    21(183) -> 184*
    21(143) -> 144*
    21(23) -> 24*
    21(220) -> 221*
    21(8) -> 9*
    21(165) -> 166*
    21(105) -> 106*
    11(10) -> 11*
    11(187) -> 188*
    11(162) -> 163*
    11(142) -> 143*
    11(107) -> 108*
    11(102) -> 103*
    11(57) -> 58*
    11(79) -> 80*
    11(34) -> 35*
    11(91) -> 92*
    11(168) -> 169*
    11(200) -> 201*
    31(55) -> 56*
    31(45) -> 46*
    31(30) -> 31*
    31(227) -> 228*
    31(197) -> 198*
    31(67) -> 68*
    31(47) -> 48*
    31(199) -> 200*
    31(179) -> 180*
    31(129) -> 130*
    31(119) -> 120*
    31(141) -> 142*
    31(136) -> 137*
    31(103) -> 104*
    31(78) -> 79*
    31(33) -> 34*
    31(185) -> 186*
    51(137) -> 138*
    51(219) -> 220*
    51(209) -> 210*
    51(139) -> 140*
    51(178) -> 179*
    51(153) -> 154*
    51(93) -> 94*
    51(155) -> 156*
    01(167) -> 168*
    01(127) -> 128*
    01(104) -> 105*
    01(69) -> 70*
    01(59) -> 60*
    01(9) -> 10*
    01(186) -> 187*
    01(121) -> 122*
    01(116) -> 117*
    01(56) -> 57*
    01(11) -> 12*
    01(118) -> 119*
    01(140) -> 141*
    01(90) -> 91*
    41(75) -> 76*
    41(89) -> 90*
    41(201) -> 202*
    41(163) -> 164*
    00(2) -> 4*
    00(1) -> 4*
    00(3) -> 4*
    10(2) -> 1*
    10(1) -> 1*
    10(3) -> 1*
    20(2) -> 2*
    20(1) -> 2*
    20(3) -> 2*
    30(2) -> 6*
    30(1) -> 6*
    30(3) -> 6*
    40(2) -> 3*
    40(1) -> 3*
    40(3) -> 3*
    50(2) -> 5*
    50(1) -> 5*
    50(3) -> 5*
    1 -> 153,121,45,21
    2 -> 139,116,33,7
    3 -> 155,127,47,23
    8 -> 219,89,69,30
    9 -> 178,75,55
    10 -> 93,67
    11 -> 209*
    12 -> 122,4
    22 -> 8*
    24 -> 8*
    31 -> 102,59
    32 -> 10*
    34 -> 77*
    37 -> 11*
    46 -> 34*
    48 -> 34*
    58 -> 154,165,122,5,4
    61 -> 57*
    68 -> 57*
    70 -> 136,31
    76 -> 9*
    78 -> 183*
    80 -> 36*
    91 -> 211*
    92 -> 107,60
    94 -> 57*
    106 -> 122,4
    108 -> 105*
    118 -> 129*
    120 -> 107*
    122 -> 117*
    128 -> 117*
    130 -> 162,119
    138 -> 107*
    140 -> 165*
    144 -> 105*
    154 -> 140*
    156 -> 140*
    164 -> 105*
    166 -> 220,140,185
    167 -> 199*
    169 -> 154,165,223,197,5
    180 -> 168*
    184 -> 9*
    189 -> 154,165,5
    198 -> 154,165,5
    202 -> 154,165,5
    210 -> 154,165,5
    212 -> 10*
    221 -> 227*
    222 -> 56*
    224 -> 5*
    228 -> 57*
  problem:
   
  Qed